$\forall$$k$:Knd, $T$, $B$:Type, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it tg}$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$$B$), ${\it es}$:ES.
\\[0ex]usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$) $\in$ Prop